x, tg:Id, k:Knd, l:IdLnk, T, A, B:Type.
(rcv(l,tg) = k  T = B)
 (f:(ABT).
 (@source(l): k(v) sends [tg,   a,b. [f(a,b)](x, v)] on link l    Dsys
 (& (D:Dsys.
 (& (@source(l): k(v) sends [tg,   a,b. [f(a,b)](x, v)] on link l    D
 (& ( D 
 (& ( realizes es.
 (& ( vartype(source(l);x)  A
 (& ( & (e:E. loc(e) = source(l)  Id  kind(e) = k  Knd  valtype(e)  B)
 (& ( & (e:E. kind(e) = rcv(l,tg)  Knd  valtype(e)  T)
 (& ( & (e:E.
 (& ( & (loc(e) = source(l)  Id
 (& ( & ( kind(e) = k  Knd
 (& ( & ( (e':E.
 (& ( & ( (kind(e') = rcv(l,tg)  Knd
 (& ( & ( (& sender(e') = e  E
 (& ( & ( (& & (e'':E. kind(e'') = rcv(l,tg)  Knd  sender(e'') = e  E  e'' = e'  E)
 (& ( & ( (& & val(e') = f((x when e),val(e))  T)))) 

latex

Definitions	ES, T, True, AB, A, False, hd(l), {T}, (x  l), P  Q, P  Q, sender(e), b, x when e, vartype(i;x), val(e), valtype(e), ij, Top, ||as||, x:A. B(x), E, loc(e), source(l), kind(e), ES(the_w), Id, IdLnk, Knd, rcv(l,tg), Prop, D realizes es. P(es), Dsys, D1  D2, World, FairFifo, PossibleWorld(D;w), x:A. B(x), t  T, P  Q, P & Q, A & B
Lemmas	possible-world wf, fair-fifo wf, world wf, d-sub wf, dsys wf, rcv wf, Knd wf, IdLnk wf, Id wf, s-sends-rule1, w-es wf, es-kind wf, lsrc wf, es-loc wf, es-E wf, length-map, length wf1, non neg length, es-val wf, es-when wf, es-sender wf, member singleton, es-kind-rcv, ge wf, es-vartype wf, subtype rel wf, hd wf, event system wf, true wf, squash wf